Nuprl Lemma : init-p-realizable
0,22
postcript
pdf
T
:Type,
v
:
T
,
x
,
i
:Id. AtomFree(Type;
T
)
es
.@
i
x
initially
v
:
T
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
es
.
P
(
es
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Prop
,
x
.
t
(
x
)
,
x
(
s
)
Lemmas
Rinit
wf
,
R-init-rule
,
R-realizes
wf
,
init-p
wf
,
event
system
wf
,
atom-free
wf
,
Id
wf
origin
T:Type, v:T, x, i:Id. AtomFree(Type;T) 
es.@i x initially v:T T:Type, v:T, x, i:Id. AtomFree(Type;T) es.@i x initially v:T x:A. B(x) Qes.P(es)
x:A. B(x)
T
x. t(x)